In recent years, it has become known that a method of dynamically analyzing an input/output relationship called a model inspection method is effective. The model inspection method is a method of constructing a model of a software 002 of which output value is dynamically determined according to an input value with respect to the software 002 and an internal state of the software 002 and evaluating validity of a dynamic behavior of the software 002 observed as an output value sequence output in time series from the model. Thus, the method searches for the existence of an input value or internal state corresponding to a problem violating a functional requirement and a safety requirement.
The model inspection method is a dynamic input/output relationship analysis method in the sense that the method defines an internal state value describing an internal state of the software 002 and searches for a state transition sequence corresponding to a problem by using a state transition model that implements a state transition rule corresponding to an input/output relation of the software 002. The following PTL 1 describes a technique relating to a model inspection method in the related art.
In particular, in order to speed up analysis, a software inspection apparatus 001 using a satisfiability determination function is disclosed. There is known a method using a Boolean SAT solver that makes a state value into a bit value and performs a binary tree search at a bit level and an SMT (Satisfiability Modulo Theory) solver that satisfies satisfiability using background logic.